<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Extract: Running Coq programs in ML</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: Verified Functional Algorithms</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Extract<span class="subtitle">Running Coq programs in ML</span></h1>


<div class="code code-tight">
<span class="id" type="keyword">Require</span> <span class="id" type="var">Extraction</span>.<br/>
</div>

<div class="doc">
Coq's <span class="inlinecode"><span class="id" type="var">Extraction</span></span> feature allows you to write a functional
    program inside Coq; (presumably) use Coq's logic to prove some
    correctness properties about it; then print it out as an ML (or
    Haskell) program that you can compile with your optimizing ML (or
    Haskell) compiler.

<div class="paragraph"> </div>

    The <a href="https://www.cis.upenn.edu/~bcpierce/sf/lf-current/Extraction.html"><span class="inlineref">Extraction</span></a> chapter of <i>Logical Foundations</i> gave a
    simple example of Coq's program extraction features.  In this
    chapter, we'll take a deeper look. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-extraction-inside-module". <span class="comment">(*&nbsp;turn&nbsp;off&nbsp;a&nbsp;warning&nbsp;message&nbsp;*)</span><br/>
<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Perm</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Sort1</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insert</span> (<span class="id" type="var">i</span>:<span class="id" type="var">nat</span>) (<span class="id" type="var">l</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) := <br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">i</span>::<span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">h</span>::<span class="id" type="var">t</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">i</span> &lt;=? <span class="id" type="var">h</span> <span class="id" type="keyword">then</span> <span class="id" type="var">i</span>::<span class="id" type="var">h</span>::<span class="id" type="var">t</span> <span class="id" type="keyword">else</span> <span class="id" type="var">h</span> :: <span class="id" type="var">insert</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">sort</span> (<span class="id" type="var">l</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">list</span> <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">h</span>::<span class="id" type="var">t</span> ⇒ <span class="id" type="var">insert</span> <span class="id" type="var">h</span> (<span class="id" type="var">sort</span> <span class="id" type="var">t</span>)<br/>
<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="var">Extraction</span></span> command prints out a function as Ocaml code. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="var">Coq.extraction.Extraction</span>.<br/>
<span class="id" type="var">Extraction</span> <span class="id" type="var">sort</span>.<br/>
</div>

<div class="doc">
You can see the translation of "sort" from Coq to Ocaml,
    in the "Messages" window of your IDE.
   Examine it there, and notice the similarities and differences.

<div class="paragraph"> </div>

  However, we really want the whole program, including the <span class="inlinecode"><span class="id" type="var">insert</span></span>
  function.  We get that as follows: 
</div>
<div class="code code-tight">

<span class="id" type="var">Recursive Extraction</span> <span class="id" type="var">sort</span>.<br/>
</div>

<div class="doc">
The first thing you see there is a redefinition of the <span class="inlinecode"><span class="id" type="var">bool</span></span> type.
  But Ocaml already has a <span class="inlinecode"><span class="id" type="var">bool</span></span> type whose inductive structure is
  isomorphic.  We want our extracted functions to be compatible with,
  callable by, ordinary Ocaml code.  So we want to use Ocaml's standard
  notation for the inductive definition, <span class="inlinecode"><span class="id" type="var">bool</span></span>.  The following directive
  accomplishes that: 
</div>
<div class="code code-tight">

<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">bool</span> ⇒ "bool" [ "true" "false" ].<br/>
<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">list</span> ⇒ "list" [ "[]" "(::)" ].<br/>
<span class="id" type="var">Recursive Extraction</span>  <span class="id" type="var">sort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Sort1</span>.<br/>
</div>

<div class="doc">
This is better.  But the program still uses a unary representation of
  natural numbers:  the number 7 is really (S (S (S (S (S (S (S O))))))). which in 
  Ocaml will be a data structure that's seven pointers deep.  The <span class="inlinecode"><span class="id" type="var">leb</span></span> function
  takes time proportional to the difference in value between <span class="inlinecode"><span class="id" type="var">n</span></span> and <span class="inlinecode"><span class="id" type="var">m</span></span>,
  which is terrible.  We'd like natural numbers to be represented as Ocaml <span class="inlinecode"><span class="id" type="var">int</span></span>.
  Unfortunately, there are only a finite number of <span class="inlinecode"><span class="id" type="var">int</span></span> values in Ocaml
  (2^31, or 2^63, depending on your implementation); so there are things
  you could prove about some programs, in Coq, that wouldn't be true in Ocaml.

<div class="paragraph"> </div>

  There are two solutions to this problem:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Instead of using <span class="inlinecode"><span class="id" type="var">nat</span></span>, use a more efficient constructive type, such as <span class="inlinecode"><span class="id" type="var">Z</span></span>.

</li>
<li> Instead of using <span class="inlinecode"><span class="id" type="var">nat</span></span>, use an <i>abstract type</i>, and instantiate it with
       Ocaml integers.

</li>
</ul>
  The first alternative uses Coq's <span class="inlinecode"><span class="id" type="var">Z</span></span> type, an inductive type with
  constructors <span class="inlinecode"><span class="id" type="var">xI</span></span> <span class="inlinecode"><span class="id" type="var">xH</span></span> etc.  <span class="inlinecode"><span class="id" type="var">Z</span></span> represents 7 as <span class="inlinecode"><span class="id" type="var">Zpos</span></span> <span class="inlinecode">(<span class="id" type="var">xI</span></span> <span class="inlinecode">(<span class="id" type="var">xI</span></span> <span class="inlinecode"><span class="id" type="var">xH</span>))</span>,
  that is,  +(  1+2*(  1+2*  1 )).
  A number <span class="inlinecode"><span class="id" type="var">n</span></span> is represented as a data structure of size log(n), and
  the operations (plus, less-than) also take about log(n) each.

<div class="paragraph"> </div>

  <span class="inlinecode"><span class="id" type="var">Z</span></span>'s log-time per operation is much better than linear time; but in
  Ocaml we are used to having constant-time operations.  Thus, here
  we will explore the second alternative: program with abstract types,
  then use an extraction directive to get efficiency. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ZArith</span>.<br/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">Z_scope</span>.<br/>
</div>

<div class="doc">
We will be using <span class="inlinecode"><span class="id" type="keyword">Parameter</span></span> and <span class="inlinecode"><span class="id" type="keyword">Axiom</span></span> in Coq.   You already saw
 these keywords, in a <span class="inlinecode"><span class="id" type="keyword">Module</span></span> <span class="inlinecode"><span class="id" type="keyword">Type</span></span>, in the <a href="ADT.html"><span class="inlineref">ADT</span></a> chapter.
 There, they describe interface components that must be instantiated
 by any <span class="inlinecode"><span class="id" type="keyword">Module</span></span> that satisfies the type.  Here, we will use this
 feature in a different (and more dangerous) way:  To axiomatize
 a mathematical theory without actually constructing it.  The reason
 that's dangerous is that if your axioms are inconsistent, then you
 can prove <span class="inlinecode"><span class="id" type="var">False</span></span>, or in fact, you can prove <i>anything</i>, so all your
 proofs are worthless.  So we must take care!  

<div class="paragraph"> </div>

 Here, we will axiomatize a <i>very weak</i> mathematical theory:  
 We claim that there exists some type <span class="inlinecode"><span class="id" type="var">int</span></span> with a function <span class="inlinecode"><span class="id" type="var">ltb</span></span>, 
 so that <span class="inlinecode"><span class="id" type="var">int</span></span> injects into <span class="inlinecode"><span class="id" type="var">Z</span></span>, and <span class="inlinecode"><span class="id" type="var">ltb</span></span> corresponds to the &lt; relation
 on Z.  That seems true enough (for example, take <span class="inlinecode"><span class="id" type="var">int</span>=<span class="id" type="var">Z</span></span>), but
 we're not <i>proving</i> it here. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">int</span> : <span class="id" type="keyword">Type</span>. <span class="comment">(*&nbsp;This&nbsp;is&nbsp;the&nbsp;Ocaml&nbsp;<span class="inlinecode"><span class="id" type="var">int</span></span>&nbsp;type.&nbsp;*)</span><br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Inlined</span> <span class="id" type="var">Constant</span> <span class="id" type="var">int</span> ⇒ "int". <span class="comment">(*&nbsp;so,&nbsp;extract&nbsp;it&nbsp;that&nbsp;way!&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Parameter</span> <span class="id" type="var">ltb</span>: <span class="id" type="var">int</span> → <span class="id" type="var">int</span> → <span class="id" type="var">bool</span>. <span class="comment">(*&nbsp;This&nbsp;is&nbsp;the&nbsp;Ocaml&nbsp;(&lt;)&nbsp;operator.&nbsp;*)</span><br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Inlined</span> <span class="id" type="var">Constant</span> <span class="id" type="var">ltb</span> ⇒ "(&lt;)". <span class="comment">(*&nbsp;so,&nbsp;extract&nbsp;it&nbsp;that&nbsp;way!&nbsp;*)</span><br/>
</div>

<div class="doc">
Now, we need to axiomatize <span class="inlinecode"><span class="id" type="var">ltb</span></span> so that we can reason about 
  programs that use it.  We need to take great care here: the
  axioms had better be consistent with Ocaml's behavior, otherwise
  our proofs will be meaningless.

<div class="paragraph"> </div>

  One axiomatization of <span class="inlinecode"><span class="id" type="var">ltb</span></span> is just that it's a total order, irreflexive
  and transitive.  This would work just fine.  But instead, I choose to
  claim that there's an injection from "int" into the mathematical integers,
  Coq's <span class="inlinecode"><span class="id" type="var">Z</span></span> type.  The reason to do this is then we get to use the <span class="inlinecode"><span class="id" type="tactic">omega</span></span>
  tactic, and other Coq libraries about integer comparisons. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">int2Z</span>: <span class="id" type="var">int</span> → <span class="id" type="var">Z</span>.<br/>
<span class="id" type="keyword">Axiom</span> <span class="id" type="var">ltb_lt</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">int</span>, <span class="id" type="var">ltb</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> = <span class="id" type="var">true</span> ↔ <span class="id" type="var">int2Z</span> <span class="id" type="var">n</span> &lt; <span class="id" type="var">int2Z</span> <span class="id" type="var">m</span>.<br/>
</div>

<div class="doc">
Both of these axioms are sound.  There does (abstractly) exist a
  function from "int" to <span class="inlinecode"><span class="id" type="var">Z</span></span>, and that function <i>is</i> consistent with
  the <span class="inlinecode"><span class="id" type="var">ltb_lt</span></span> axiom.  But you should think about this until you are
  convinced.

<div class="paragraph"> </div>

  Notice that we do not give extraction directives for <span class="inlinecode"><span class="id" type="var">int2Z</span></span> or <span class="inlinecode"><span class="id" type="var">ltb_lt</span></span>.
  That's because they will not appear in <i>programs</i>, only in proofs that
  are not meant to be extracted.

<div class="paragraph"> </div>

  Now, here's a dangerous axiom:

<div class="paragraph"> </div>

  <span class="inlinecode"><span class="id" type="keyword">Parameter</span></span> <span class="inlinecode"><span class="id" type="var">ocaml_plus</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">int</span>.</span>

<div class="paragraph"> </div>

  <span class="inlinecode"><span class="id" type="var">Extract</span></span> <span class="inlinecode"><span class="id" type="var">Inlined</span></span> <span class="inlinecode"><span class="id" type="var">Constant</span></span> <span class="inlinecode"><span class="id" type="var">ocaml_plus</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode">"(+)".</span>

<div class="paragraph"> </div>

  <span class="inlinecode"><span class="id" type="keyword">Axiom</span></span> <span class="inlinecode"><span class="id" type="var">ocaml_plus_plus</span>:</span>
     <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span><span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">c</span>:</span> <span class="inlinecode"><span class="id" type="var">int</span>,</span>
       <span class="inlinecode"><span class="id" type="var">ocaml_plus</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">↔</span> <span class="inlinecode"><span class="id" type="var">int2Z</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">int2Z</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">int2Z</span></span> <span class="inlinecode"><span class="id" type="var">c</span>.</span>

<div class="paragraph"> </div>

  The first two lines are OK:  there really is a "+" function in Ocaml,
  and its type really is  <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">int</span></span>.  

<div class="paragraph"> </div>

  But <span class="inlinecode"><span class="id" type="var">ocaml_plus_plus</span></span> is unsound!   From it, you could prove,

<div class="paragraph"> </div>

  <span class="inlinecode">(<span class="id" type="var">int2Z</span></span> <span class="inlinecode"><span class="id" type="var">max_int</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">int2Z</span></span> <span class="inlinecode"><span class="id" type="var">max_int</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">int2Z</span></span> <span class="inlinecode">(<span class="id" type="var">ocaml_plus</span></span> <span class="inlinecode"><span class="id" type="var">max_int</span></span> <span class="inlinecode"><span class="id" type="var">max_int</span>)</span>,

<div class="paragraph"> </div>

  which is not true in Ocaml, because overflow wraps around, modulo
  <span class="inlinecode">2^(<span class="id" type="var">wordsize</span>-1)</span>.

<div class="paragraph"> </div>

  So we won't axiomatize Ocaml addition. 
<div class="paragraph"> </div>

<a name="lab95"></a><h1 class="section">Utilities for OCaml Integer Comparisons</h1>

<div class="paragraph"> </div>

 Just like in Perm.v, but for <span class="inlinecode"><span class="id" type="var">int</span></span> and <span class="inlinecode"><span class="id" type="var">Z</span></span> instead of <span class="inlinecode"><span class="id" type="var">nat</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">int_blt_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">int2Z</span> <span class="id" type="var">x</span> &lt; <span class="id" type="var">int2Z</span> <span class="id" type="var">y</span>) (<span class="id" type="var">ltb</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ltb_lt</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">Z_eqb_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">x</span>=<span class="id" type="var">y</span>) (<span class="id" type="var">Z.eqb</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Z.eqb_eq</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">Z_ltb_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">x</span>&lt;<span class="id" type="var">y</span>) (<span class="id" type="var">Z.ltb</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Z.ltb_lt</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Add&nbsp;these&nbsp;three&nbsp;lemmas&nbsp;to&nbsp;the&nbsp;Hint&nbsp;database&nbsp;for&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span>,<br/>
&nbsp;&nbsp;so&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span>&nbsp;tactic&nbsp;will&nbsp;work&nbsp;with&nbsp;them.&nbsp;*)</span><br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">int_blt_reflect</span> <span class="id" type="var">Z_eqb_reflect</span> <span class="id" type="var">Z_ltb_reflect</span> : <span class="id" type="var">bdestruct</span>.<br/>
</div>

<div class="doc">
<a name="lab96"></a><h1 class="section">SearchTrees, Extracted</h1>

<div class="paragraph"> </div>

 Let us re-do binary search trees, but with Ocaml integers instead of  Coq nats. 
<div class="paragraph"> </div>

<a name="lab97"></a><h2 class="section">Maps, on <span class="inlinecode"><span class="id" type="var">Z</span></span> Instead of <span class="inlinecode"><span class="id" type="var">nat</span></span></h2>
 Our original proof with nats used <span class="inlinecode"><span class="id" type="var">Maps.total_map</span></span> in its abstraction relation,
     but that won't work here because we need maps over <span class="inlinecode"><span class="id" type="var">Z</span></span> rather than <span class="inlinecode"><span class="id" type="var">nat</span></span>.
     So, we copy-paste-edit to make <span class="inlinecode"><span class="id" type="var">total_map</span></span> over <span class="inlinecode"><span class="id" type="var">Z</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Coq.Logic.FunctionalExtensionality</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">IntMaps</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">total_map</span> (<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>) := <span class="id" type="var">Z</span> → <span class="id" type="var">A</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">t_empty</span> {<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">v</span> : <span class="id" type="var">A</span>) : <span class="id" type="var">total_map</span> <span class="id" type="var">A</span> :=  (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">v</span>).<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">t_update</span> {<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">m</span> : <span class="id" type="var">total_map</span> <span class="id" type="var">A</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">Z</span>) (<span class="id" type="var">v</span> : <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x'</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">Z.eqb</span> <span class="id" type="var">x</span> <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">v</span> <span class="id" type="keyword">else</span> <span class="id" type="var">m</span> <span class="id" type="var">x'</span>.<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">t_update_eq</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">A</span> (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">A</span>) <span class="id" type="var">x</span> <span class="id" type="var">v</span>, (<span class="id" type="var">t_update</span> <span class="id" type="var">m</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span>) <span class="id" type="var">x</span> = <span class="id" type="var">v</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x</span>=?<span class="id" type="var">x</span>); <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">t_update_neq</span> : <span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) <span class="id" type="var">v</span> <span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">x<sub>2</sub></span> (<span class="id" type="var">m</span> : <span class="id" type="var">total_map</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">x<sub>1</sub></span> ≠ <span class="id" type="var">x<sub>2</sub></span> →  (<span class="id" type="var">t_update</span> <span class="id" type="var">m</span> <span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">v</span>) <span class="id" type="var">x<sub>2</sub></span> = <span class="id" type="var">m</span> <span class="id" type="var">x<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x<sub>1</sub></span>=?<span class="id" type="var">x<sub>2</sub></span>); <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">t_update_shadow</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">A</span> (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">A</span>) <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t_update</span> (<span class="id" type="var">t_update</span> <span class="id" type="var">m</span> <span class="id" type="var">x</span> <span class="id" type="var">v<sub>1</sub></span>) <span class="id" type="var">x</span> <span class="id" type="var">v<sub>2</sub></span>  = <span class="id" type="var">t_update</span> <span class="id" type="var">m</span> <span class="id" type="var">x</span> <span class="id" type="var">v<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x</span>=?<span class="id" type="var">x'</span>); <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">IntMaps</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">IntMaps</span>.<br/>
</div>

<div class="doc">
<a name="lab98"></a><h2 class="section">Trees, on <span class="inlinecode"><span class="id" type="var">int</span></span> Instead of <span class="inlinecode"><span class="id" type="var">nat</span></span></h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">SearchTree2</span>.<br/>
<span class="id" type="keyword">Section</span> <span class="id" type="var">TREES</span>.<br/>
<span class="id" type="keyword">Variable</span> <span class="id" type="var">V</span> : <span class="id" type="keyword">Type</span>.<br/>
<span class="id" type="keyword">Variable</span> <span class="id" type="var">default</span>: <span class="id" type="var">V</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">key</span> := <span class="id" type="var">int</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tree</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;| <span class="id" type="var">E</span> : <span class="id" type="var">tree</span><br/>
&nbsp;| <span class="id" type="var">T</span>: <span class="id" type="var">tree</span> → <span class="id" type="var">key</span> → <span class="id" type="var">V</span> → <span class="id" type="var">tree</span> → <span class="id" type="var">tree</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty_tree</span> : <span class="id" type="var">tree</span> := <span class="id" type="var">E</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">lookup</span> (<span class="id" type="var">x</span>: <span class="id" type="var">key</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">tree</span>) : <span class="id" type="var">V</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">default</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">tl</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">tr</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">ltb</span> <span class="id" type="var">x</span> <span class="id" type="var">k</span> <span class="id" type="keyword">then</span> <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">tl</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">ltb</span> <span class="id" type="var">k</span> <span class="id" type="var">x</span> <span class="id" type="keyword">then</span> <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">tr</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">v</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insert</span> (<span class="id" type="var">x</span>: <span class="id" type="var">key</span>) (<span class="id" type="var">v</span>: <span class="id" type="var">V</span>) (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) : <span class="id" type="var">tree</span> :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">s</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">T</span> <span class="id" type="var">E</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">E</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">y</span> <span class="id" type="var">v'</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="keyword">if</span>  <span class="id" type="var">ltb</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">T</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">a</span>) <span class="id" type="var">y</span> <span class="id" type="var">v'</span> <span class="id" type="var">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">ltb</span> <span class="id" type="var">y</span> <span class="id" type="var">x</span> <span class="id" type="keyword">then</span> <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">y</span> <span class="id" type="var">v'</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">elements'</span> (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) (<span class="id" type="var">base</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) : <span class="id" type="var">list</span> (<span class="id" type="var">key</span> * <span class="id" type="var">V</span>) :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">s</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">base</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="var">elements'</span> <span class="id" type="var">a</span> ((<span class="id" type="var">k</span>,<span class="id" type="var">v</span>) :: <span class="id" type="var">elements'</span> <span class="id" type="var">b</span> <span class="id" type="var">base</span>)<br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">elements</span> (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) : <span class="id" type="var">list</span> (<span class="id" type="var">key</span> * <span class="id" type="var">V</span>) := <span class="id" type="var">elements'</span> <span class="id" type="var">s</span> <span class="id" type="var">nil</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">combine</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">pivot</span>: <span class="id" type="var">Z</span>) (<span class="id" type="var">m<sub>1</sub></span> <span class="id" type="var">m<sub>2</sub></span>: <span class="id" type="var">total_map</span> <span class="id" type="var">A</span>) : <span class="id" type="var">total_map</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">Z.ltb</span> <span class="id" type="var">x</span> <span class="id" type="var">pivot</span>  <span class="id" type="keyword">then</span> <span class="id" type="var">m<sub>1</sub></span> <span class="id" type="var">x</span> <span class="id" type="keyword">else</span> <span class="id" type="var">m<sub>2</sub></span> <span class="id" type="var">x</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">Abs</span>:  <span class="id" type="var">tree</span> → <span class="id" type="var">total_map</span> <span class="id" type="var">V</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">Abs_E</span>: <span class="id" type="var">Abs</span> <span class="id" type="var">E</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>)<br/>
| <span class="id" type="var">Abs_T</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">l</span> <span class="id" type="var">a</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">r</span> <span class="id" type="var">b</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">T</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span>)  (<span class="id" type="var">t_update</span> (<span class="id" type="var">combine</span> (<span class="id" type="var">int2Z</span> <span class="id" type="var">k</span>) <span class="id" type="var">a</span> <span class="id" type="var">b</span>) (<span class="id" type="var">int2Z</span> <span class="id" type="var">k</span>) <span class="id" type="var">v</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">empty_tree_relate</span>: <span class="id" type="var">Abs</span> <span class="id" type="var">empty_tree</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">constructor</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab99"></a><h4 class="section">Exercise: 3 stars (lookup_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lookup_relate</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> ,   <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> =  <span class="id" type="var">cts</span> (<span class="id" type="var">int2Z</span> <span class="id" type="var">k</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;Copy&nbsp;your&nbsp;proof&nbsp;from&nbsp;SearchTree.v,&nbsp;and&nbsp;adapt&nbsp;it.&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab100"></a><h4 class="section">Exercise: 3 stars (insert_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">insert_relate</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">insert</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span>) (<span class="id" type="var">t_update</span> <span class="id" type="var">cts</span> (<span class="id" type="var">int2Z</span> <span class="id" type="var">k</span>) <span class="id" type="var">v</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;Copy&nbsp;your&nbsp;proof&nbsp;from&nbsp;SearchTree.v,&nbsp;and&nbsp;adapt&nbsp;it.&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab101"></a><h4 class="section">Exercise: 1 star (unrealistically_strong_can_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">unrealistically_strong_can_relate</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span>,  <span style='font-size:120%;'>&exist;</span> <span class="id" type="var">cts</span>, <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;Copy-paste&nbsp;your&nbsp;proof&nbsp;from&nbsp;SearchTree.v;&nbsp;it&nbsp;should&nbsp;work&nbsp;as&nbsp;is.&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">TREES</span>.<br/>
</div>

<div class="doc">
Now, run this command and examine the results in the "results"
   window of your IDE: 
</div>
<div class="code code-tight">

<span class="id" type="var">Recursive Extraction</span> <span class="id" type="var">empty_tree</span> <span class="id" type="var">insert</span> <span class="id" type="var">lookup</span> <span class="id" type="var">elements</span>.<br/>
</div>

<div class="doc">
Next, we will extract it into an Ocaml source file, and measure its 
  performance. 
</div>
<div class="code code-tight">

<span class="id" type="var">Extraction</span> "searchtree.ml" <span class="id" type="var">empty_tree</span> <span class="id" type="var">insert</span> <span class="id" type="var">lookup</span> <span class="id" type="var">elements</span>.<br/>
</div>

<div class="doc">
Note: we've done the extraction <i>inside</i> the module, even though
   Coq warns against it, for a specific reason:  We want to extract only
   the program, not the proofs. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">SearchTree2</span>.<br/>
</div>

<div class="doc">
<a name="lab102"></a><h1 class="section">Performance Tests</h1>

<div class="paragraph"> </div>

 Read the Ocaml program, test_searchtree.ml:
<pre>
let test (f: int -&gt; int) (n: int) =
 let rec build (j, t) = if j=0 then t
                    else build(j-1, insert (f j) 1 t)
  in let t<sub>1</sub> = build(n,empty_tree)
  in let rec g (j,count) = if j=0 then count
                       else if lookup 0 (f j) t<sub>1</sub> = 1
                            then g(j-1,count+1)
                            else g(j-1,count)
  in let start = Sys.time()
  in let answer = g(n,0)
      in (answer, Sys.time() -. start)

let print_test name (f: int -&gt; int) n =
  let (answer, time) = test f n
  in (print_string "Insert and lookup "; print_int n;
      print_string " "; print_string name; print_string " integers in ";
      print_float time; print_endline " seconds.")
  
let test_random n = print_test "random" (fun _ -&gt; Random.int n) n
let test_consec n = print_test "consecutive" (fun i -&gt; n-i) n

let run_tests() = (test_random 1000000; test_random 20000; test_consec 20000)
		    
let _ = run_tests ()
</pre>
 
<div class="paragraph"> </div>

 You can run this inside the ocaml top level by:
<pre>
#use "searchtree.ml";;
#use "test_searchtree.ml";;
run_tests();;
</pre>

<div class="paragraph"> </div>

On my machine, in the byte-code interpreter this prints,

<div class="paragraph"> </div>

<pre>
Insert and lookup 1000000 random integers in 1.076 seconds.
Insert and lookup 20000 random integers in 0.015 seconds.
Insert and lookup 20000 consecutive integers in 5.054 seconds.
</pre>

<div class="paragraph"> </div>

You can compile and run this with the ocaml native-code compiler by:
<pre>
ocamlopt searchtree.mli searchtree.ml -open Searchtree test_searchtree.ml -o test_searchtree
./test_searchtree
</pre>

<div class="paragraph"> </div>

On my machine this prints,
<pre>
Insert and lookup 1000000 random integers in 0.468 seconds.
Insert and lookup 20000 random integers in 0. seconds.
Insert and lookup 20000 consecutive integers in 0.374 seconds.
</pre>

<div class="paragraph"> </div>

<a name="lab103"></a><h1 class="section">Unbalanced Binary Search Trees</h1>
 Why is the performance of the algorithm so much worse when the
   keys are all inserted consecutively?  To examine this, let's compute
   with some searchtrees inside Coq.  We cannot do this with the search
   trees defined thus far in this file, because they use a key-comparison
   function <span class="inlinecode"><span class="id" type="var">ltb</span></span>  that is abstract and uninstantiated (only during
   Extraction to Ocaml does <span class="inlinecode"><span class="id" type="var">ltb</span></span> get instantiated).

<div class="paragraph"> </div>

   So instead, we'll use the SearchTree module, 
   where everything runs inside Coq. 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="var">SearchTree</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Experiments</span>.<br/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">nat_scope</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty_tree</span> := <span class="id" type="var">SearchTree.empty_tree</span> <span class="id" type="var">nat</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">insert</span> := <span class="id" type="var">SearchTree.insert</span> <span class="id" type="var">nat</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">lookup</span> := <span class="id" type="var">SearchTree.lookup</span> <span class="id" type="var">nat</span> 0.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">E</span> := <span class="id" type="var">SearchTree.E</span> <span class="id" type="var">nat</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">T</span> := <span class="id" type="var">SearchTree.T</span> <span class="id" type="var">nat</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Goal</span> <span class="id" type="var">insert</span> 5 1 (<span class="id" type="var">insert</span> 4 1 (<span class="id" type="var">insert</span> 3 1 (<span class="id" type="var">insert</span> 2 1 (<span class="id" type="var">insert</span> 1 1 (<span class="id" type="var">insert</span> 0 1 <span class="id" type="var">empty_tree</span>))))) ≠ <span class="id" type="var">E</span>.<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="var">fold</span> <span class="id" type="var">E</span>; <span class="id" type="tactic">repeat</span> <span class="id" type="var">fold</span> <span class="id" type="var">T</span>.<br/>
</div>

<div class="doc">
Look here!  The tree is completely unbalanced.  Looking up <span class="inlinecode">5</span> will take linear time.
   That's why the runtime on consecutive integers is so bad. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a name="lab104"></a><h1 class="section">Balanced Binary Search Trees</h1>

<div class="paragraph"> </div>

 To achieve robust performance (that stays N log N for a sequence
    of N operations, and does not degenerate to N*N), we must keep the
    search trees balanced.  The next chapter, <a href="Redblack.html"><span class="inlineref">Redblack</span></a>,
    implements that idea. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Experiments</span>.<br/>
</div>
</div>



</div>

</body>
</html>